es-secret-server{$table:ut2, $encrypt:ut2, $decrypt:ut2}
es-secret-server(es; T; L; i)
== let ds = "$table" : secret-table(T) in 
== (lL.
== (destination(l) = i
== (& state ds
== (& rcv(l,"$encrypt"):(+Atom1)
== (& rcv(l,"$encrypt"):data(T) sends ["$encrypt", e.next("$table" when e):Atom1] on lnk-inv(l)
== (& state ds
== (& rcv(l,"$decrypt"):(+Atom1)
== (& rcv(l,"$decrypt"):Atom1 sends ["$decrypt", e.decrypt("$table" when e;val(e)):data(T)] on lnk-inv(l))
== & @i only events in map(l.rcv(l,"$encrypt");L) change   "$table" : secret-table(T)
== & & (lL.
== & & (@i 
== & & (@i events of kind rcv(l,"$encrypt") change "$table" to
== & & (@i es,v. encrypt(s."$table";v) State(ds) (val:(+Atom1)data(T)))
== & & & e@i.
== & & & e':E.
== & & & e leaks "$table" to e'
== & & &  (lL.kind(e) = rcv(l,"$encrypt") & kind(e') = rcv(lnk-inv(l),"$encrypt")
== & & &   kind(e) = rcv(l,"$decrypt") & kind(e') = rcv(lnk-inv(l),"$decrypt"))
== & & & e@i. e copies "$table"
== & & & e@i.
== & & & first(e)
== & & &  atoms-distinct("$table" when e)
== & & &  & ptr("$table" when e) = 0
== & & &  & (n:, j:Id. n<||"$table" when e||   j >> st-atom("$table" when e;n)  j = i) 

latex

---

clarification:

es-secret-server{$table:ut2, $encrypt:ut2, $decrypt:ut2}
es-secret-server(es; T; L; i)
== let ds = "$table" : secret-table(T) in 
== l_all(L;IdLnk;l.destination(l) = i  Id
== & es-kind-sends-iff(es;rcv(l,"$encrypt");(+Atom1)
== & es-kind-sends-iff(es;rcv(l,"$encrypt");data(T);lnk-inv(l);"$encrypt";Atom1;ds;e.next(es-when
== (es; "$table"; e)))
== & es-kind-sends-iff(es;rcv(l,"$decrypt");(+Atom1)
== & es-kind-sends-iff(es;rcv(l,"$decrypt");Atom1;lnk-inv(l);"$decrypt";data(T);ds;e.decrypt(es-when
== & (es; "$table"; e);es-val(es; e))))
== & frame-p(es; i; secret-table(T); "$table"; map(l.rcv(l,"$encrypt");L))
== & & l_all(L;IdLnk;l.effect-p(es;i;ds;rcv(l,"$encrypt");(+Atom1)data(T);"$table";s,v.
== & & encrypt(s."$table";v)))
== & & & alle-at(es;i;e.e':es-E(es).
== & & es-leaks(es;e;"$table";e')
== & &  l_exists(L;IdLnk;l.es-kind(es; e) = rcv(l,"$encrypt")  Knd
== & &  & es-kind(es; e') = rcv(lnk-inv(l),"$encrypt")  Knd
== & &   es-kind(es; e) = rcv(l,"$decrypt")  Knd
== & &   & es-kind(es; e') = rcv(lnk-inv(l),"$decrypt")  Knd))
== & & & alle-at(es;i;e.es-copies(es;e;"$table"))
== & & & alle-at(es;i;e.es-first(es; e)
== & & & alle-at(es;i;e. atoms-distinct(es-when(es; "$table"; e))
== & & & alle-at(es;i;e. & ptr(es-when(es; "$table"; e)) = 0  
== & & & alle-at(es;i;e. & (n:, j:Id.
== & & & alle-at(es;i;e. & (n<||es-when(es; "$table"; e)|| 
== & & & alle-at(es;i;e. & ( es-atom(es;j;st-atom(es-when(es; "$table"; e);n))
== & & & alle-at(es;i;e. & ( j = i  Id)) 

latex

Definitions

let x = a in b(x), x : v, destination(l), next(tab), state dsk:A sends [tg, e.f(e):B] on l, decrypt(tab;kval), val(e), A & B, @i only events in L change   x : T, secret-table(T), map(f;as), xL. P(x), @i events of kind k change x to f State(ds) (val:T), x:AB(x), left+right, Atom$n, data(T), x.A(x), encrypt(tab;keyv), s.x, x:A. B(x), E, e leaks x to e', (xL.P(x)), IdLnk, P  Q, Knd, kind(e), rcv(l,tg), lnk-inv(l), A, e copies x, e@i. P(e), b, first(e), atoms-distinct(tab), P & Q, ptr(tab), #$n, , x:A. B(x), a<b, ||tab|| , P  Q, i >> a, st-atom(tab;n), x when e, "$x", s = t, Id